<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue7815</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">module</a> <a id="8" href="Issue7815.html" class="Module">Issue7815</a> <a id="18" class="Keyword">where</a>
<a id="24" class="Keyword">module</a> <a id="X"></a><a id="31" href="Issue7815.html#31" class="Module">X</a> <a id="33" class="Keyword">where</a>
<a id="39" class="Keyword">module</a> <a id="46" href="Issue7815.html#46" class="Module">_</a>
  <a id="50" class="Symbol">(</a><a id="51" href="Issue7815.html#51" class="Bound">a</a> <a id="53" class="Symbol">:</a> <a id="55" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="58" class="Symbol">)</a> <a id="60" class="Comment">-- Before fixing issue 7815, `a` and `Set` were not highlighted.</a>
  <a id="127" class="Symbol">(</a><a id="128" class="Keyword">let</a> <a id="132" class="Keyword">module</a> <a id="139" href="Issue7815.html#139" class="Module">Y</a> <a id="141" class="Symbol">=</a> <a id="143" href="Issue7815.html#31" class="Module">X</a><a id="144" class="Symbol">)</a>
  <a id="148" class="Keyword">where</a>
</pre></body></html>